$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $f$:$a$:$A$ fp$\rightarrow$ Top. fpf{-}dom{-}list($f$) $\in$ (\{$a$:$A$$\mid$ $\uparrow$$a$ $\in$ dom($f$)\}  List)